$\forall$$A$:Type, ${\it es}$:ES, $I$:AbsInterface($A$), $P$:(E$\rightarrow\mathbb{P}$), $p$:($\forall$$e$:E. Dec($P$($e$))), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ ($I$$\mid\neg$$p$))) $\Leftarrow\!\Rightarrow$ (($\uparrow$($e$ $\in_{b}$ $I$)) \& ($\neg$$P$($e$)))